x:(), r:, k:, y:( List).
(k  ||y||)
 x(k) < 0
 (q-rel(r;q-linear(k;j.x(j);y))
  q-rel(r;-(y[(k - 1)]) + ((-1/x(k)) * q-linear(k - 1;j.x(j);y)))) 

latex

Definitions

r * s, ff, tt, if b then t else f fi , q-rel(r;x), (r/s), P & Q, False, x. t(x), t  T, True, T, , P  Q, A, P  Q, A  B, P  Q, , x:A. B(x), Unit, , x(s), , , S  T

Lemmas

qmul assoc, qmul-qdiv-cancel3, qinv inv q, qmul over minus qrng, qadd comm q, qmul-qdiv-cancel4, qmul over plus qrng, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, qmul preserves qless, qle wf, qmul preserves qle, not wf, bnot wf, bool wf, eq int wf, qmul one qrng, qinv wf, assert-qeq, qeq wf2, assert wf, not functionality wrt iff, qmul zero qrng, qless-minus, qinv-negative, qless irreflexivity, qle weakening eq qorder, qless transitivity 2 qorder, nat plus wf, length wf1, nat plus inc, qless wf, le wf, q-linear wf, qdiv wf, select wf, int inc rationals, qmul wf, qadd wf, nat wf, q-linear-unroll, rationals wf, q-rel wf, true wf, squash wf, iff wf